\begin{tabbing}
$\forall$$x_{1}$:Realizer.
\\[0ex]Rsends?($x_{1}$)
\\[0ex]$\Rightarrow$ \=Rsends{-}g($x_{1}$)\+
\\[0ex]$\in$ (\=${\it tg}$:Id\+
\\[0ex]$\times$(State(Rsends{-}ds($x_{1}$))$\rightarrow$Rsends{-}T($x_{1}$)$\rightarrow$(DeclaredType(Rsends{-}dt($x_{1}$);${\it tg}$) List))) List
\-\-
\end{tabbing}